\begin{tabbing}
$\forall$${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $A$:ecl{-}trans{-}tuple\=\{i:l\}\+
\\[0ex](${\it ds}$; ${\it da}$).
\-\\[0ex]ecl{-}trans{-}a($A$)
\\[0ex]$\in$ $\mathbb{N}\rightarrow$(\=$k$:\{$k$:Knd$\mid$ ($k$ $\in$ ecl{-}trans{-}ks($A$))\} $\rightarrow$decl{-}state(${\it ds}$)$\rightarrow$ma{-}valtype(${\it da}$; $k$)$\rightarrow$\+
\\[0ex]ecl{-}trans{-}type($A$)$\rightarrow\mathbb{B}$)
\-
\end{tabbing}